Iof proof for Lemma mul cancel in eq:
1. a :
2. b :
3.
4. m :
5. (m * a) = (m * b)
a = b
by ((((Thin 3)
CollapseTHEN (Assert (a > b) 
(a = b) (a < b)))
)
CollapseTHENA (
C(Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t) inil_term)))
C1:
C1: 3. m :
C1: 4. (m * a) = (m * b)
C1: 5. (a > b) (a = b) (a < b)
C1: a = b
C.
T